<html>
<head><meta charset="utf-8"><title>Universes vs Debruijn Indices · t-compiler/help · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/index.html">t-compiler/help</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html">Universes vs Debruijn Indices</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="165202703"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165202703" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Declan Kelly <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165202703">(May 08 2019 at 21:26)</a>:</h4>
<p>Hello, can anyone explain the differences between <a href="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/struct.UniverseIndex.html" target="_blank" title="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/struct.UniverseIndex.html">universes</a> and <a href="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/struct.DebruijnIndex.html" target="_blank" title="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/struct.DebruijnIndex.html">debruijn indices</a>? Superficially it seems that they play similar roles, counting up from a binder.</p>



<a name="165203309"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165203309" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Declan Kelly <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165203309">(May 08 2019 at 21:33)</a>:</h4>
<p>My initial thought is that debruijn indices represent quantification inside of a type, while the universes can represent quantification spanning multiple types, such as inside of an impl block.</p>



<a name="165225955"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165225955" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Declan Kelly <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165225955">(May 09 2019 at 05:41)</a>:</h4>
<p>Also how does the use of <a href="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/struct.BoundVar.html" target="_blank" title="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/struct.BoundVar.html">bounds vars</a> play into this? From the TyKind docs I see that placeholder types are a <code>Placeholder&lt;BoundVar&gt;</code> where <code>Placeholder</code> contains a <code>UniverseIndex</code>. What kind of data is <code>BoundVar</code> associated with, and in what context is <code>TyKind::Placeholder</code> used? Would it just be the <code>T</code> in <code>fn identity&lt;T&gt;(data: T) -&gt; T {}</code>?</p>



<a name="165292329"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165292329" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165292329">(May 09 2019 at 22:00)</a>:</h4>
<p><span class="user-mention" data-user-id="129532">@Declan Kelly</span> you might want to read <a href="https://rust-lang.github.io/rustc-guide/borrow_check/region_inference.html#placeholders-and-universes" target="_blank" title="https://rust-lang.github.io/rustc-guide/borrow_check/region_inference.html#placeholders-and-universes">Placeholders and universes</a> in the rustc guide</p>



<a name="165292558"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165292558" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165292558">(May 09 2019 at 22:04)</a>:</h4>
<p>see also the docs on <a href="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/enum.RegionKind.html" target="_blank" title="https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/enum.RegionKind.html"><code>RegionKind</code></a></p>



<a name="165292750"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165292750" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165292750">(May 09 2019 at 22:08)</a>:</h4>
<p>I have a hard time keeping all these straight myself, though :)</p>



<a name="165292854"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165292854" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165292854">(May 09 2019 at 22:10)</a>:</h4>
<p>I believe the <code>T</code> in your example would be a <code>BoundVar</code>, whereas universes are used to represent quantifiers (like <code>for&lt;'a&gt;</code> in <code>for&lt;'a&gt; fn (&amp;'a u32)</code>)</p>



<a name="165292858"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165292858" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165292858">(May 09 2019 at 22:10)</a>:</h4>
<p>cc <span class="user-mention" data-user-id="116009">@nikomatsakis</span></p>



<a name="165299201"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165299201" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Declan Kelly <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165299201">(May 10 2019 at 00:24)</a>:</h4>
<p><span class="user-mention" data-user-id="116883">@tmandry</span> Thank you for the help!</p>



<a name="165551163"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/182449-t-compiler/help/topic/Universes%20vs%20Debruijn%20Indices/near/165551163" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/182449-t-compiler/help/topic/Universes.20vs.20Debruijn.20Indices.html#165551163">(May 13 2019 at 17:46)</a>:</h4>
<p>The distinction is a matter of "point of view". When you are looking at some term (i.e., a type, where-clause, etc), it may have bound regions:</p>
<div class="codehilite"><pre><span></span><span class="k">for</span><span class="o">&lt;</span><span class="na">&#39;a</span><span class="o">&gt;</span><span class="w"> </span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&lt;</span><span class="na">&#39;a</span><span class="o">&gt;</span><span class="w"></span>
</pre></div>


<p>Here, <code>'a</code> would be represented with a debruijn index. But when we "enter" into that binder, we have to replace the bound region (<code>'a</code>) with something. We would replace <code>'a</code> with a placeholder that has a universe (say <code>!1</code>). In that case, we have <code>T: Foo&lt;!1&gt;</code> as our term</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>